Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar14/CimeSLASHtree.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

BS₁(n₃(x, y, z)) -> GE₂(x, max₁(y))
-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))
GE₂(1₁(x), 0₁(y)) -> GE₂(x, y)
GE₂(0₁(x), 1₁(y)) -> GE₂(y, x)
SIZE₁(n₃(x, y, z)) -> +¹₂(+₂(size₁(x), size₁(y)), 1₁(#))
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)
+¹₂(1₁(x), 1₁(y)) -> 0¹₁(+₂(+₂(x, y), 1₁(#)))
-¹₂(1₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(x, y)
SIZE₁(n₃(x, y, z)) -> +¹₂(size₁(x), size₁(y))
BS₁(n₃(x, y, z)) -> BS₁(z)
WB₁(n₃(x, y, z)) -> GE₂(1₁(#), -₂(size₁(y), size₁(z)))
WB₁(n₃(x, y, z)) -> GE₂(1₁(#), -₂(size₁(z), size₁(y)))
WB₁(n₃(x, y, z)) -> AND₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))
BS₁(n₃(x, y, z)) -> AND₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
GE₂(0₁(x), 1₁(y)) -> NOT₁(ge₂(y, x))
SIZE₁(n₃(x, y, z)) -> SIZE₁(y)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
SIZE₁(n₃(x, y, z)) -> SIZE₁(x)
WB₁(n₃(x, y, z)) -> SIZE₁(y)
WB₁(n₃(x, y, z)) -> SIZE₁(z)
BS₁(n₃(x, y, z)) -> BS₁(y)
MIN₁(n₃(x, y, z)) -> MIN₁(y)
+¹₂(0₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))
WB₁(n₃(x, y, z)) -> AND₂(wb₁(y), wb₁(z))
-¹₂(1₁(x), 1₁(y)) -> 0¹₁(-₂(x, y))
BS₁(n₃(x, y, z)) -> MAX₁(y)
WB₁(n₃(x, y, z)) -> GE₂(size₁(y), size₁(z))
+¹₂(0₁(x), 0₁(y)) -> +¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> 0¹₁(-₂(x, y))
MAX₁(n₃(x, y, z)) -> MAX₁(z)
WB₁(n₃(x, y, z)) -> -¹₂(size₁(y), size₁(z))
WB₁(n₃(x, y, z)) -> -¹₂(size₁(z), size₁(y))
BS₁(n₃(x, y, z)) -> AND₂(ge₂(x, max₁(y)), ge₂(min₁(z), x))
+¹₂(0₁(x), 0₁(y)) -> 0¹₁(+₂(x, y))
WB₁(n₃(x, y, z)) -> WB₁(z)
GE₂(1₁(x), 1₁(y)) -> GE₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> -¹₂(x, y)
WB₁(n₃(x, y, z)) -> WB₁(y)
GE₂(#, 0₁(x)) -> GE₂(#, x)
BS₁(n₃(x, y, z)) -> MIN₁(z)
BS₁(n₃(x, y, z)) -> GE₂(min₁(z), x)
BS₁(n₃(x, y, z)) -> AND₂(bs₁(y), bs₁(z))
WB₁(n₃(x, y, z)) -> IF₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y))))
GE₂(0₁(x), 0₁(y)) -> GE₂(x, y)
-¹₂(1₁(x), 1₁(y)) -> -¹₂(x, y)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BS₁(n₃(x, y, z)) -> GE₂(x, max₁(y))
-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))
GE₂(1₁(x), 0₁(y)) -> GE₂(x, y)
GE₂(0₁(x), 1₁(y)) -> GE₂(y, x)
SIZE₁(n₃(x, y, z)) -> +¹₂(+₂(size₁(x), size₁(y)), 1₁(#))
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)
+¹₂(1₁(x), 1₁(y)) -> 0¹₁(+₂(+₂(x, y), 1₁(#)))
-¹₂(1₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(x, y)
SIZE₁(n₃(x, y, z)) -> +¹₂(size₁(x), size₁(y))
BS₁(n₃(x, y, z)) -> BS₁(z)
WB₁(n₃(x, y, z)) -> GE₂(1₁(#), -₂(size₁(y), size₁(z)))
WB₁(n₃(x, y, z)) -> GE₂(1₁(#), -₂(size₁(z), size₁(y)))
WB₁(n₃(x, y, z)) -> AND₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))
BS₁(n₃(x, y, z)) -> AND₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
GE₂(0₁(x), 1₁(y)) -> NOT₁(ge₂(y, x))
SIZE₁(n₃(x, y, z)) -> SIZE₁(y)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
SIZE₁(n₃(x, y, z)) -> SIZE₁(x)
WB₁(n₃(x, y, z)) -> SIZE₁(y)
WB₁(n₃(x, y, z)) -> SIZE₁(z)
BS₁(n₃(x, y, z)) -> BS₁(y)
MIN₁(n₃(x, y, z)) -> MIN₁(y)
+¹₂(0₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))
WB₁(n₃(x, y, z)) -> AND₂(wb₁(y), wb₁(z))
-¹₂(1₁(x), 1₁(y)) -> 0¹₁(-₂(x, y))
BS₁(n₃(x, y, z)) -> MAX₁(y)
WB₁(n₃(x, y, z)) -> GE₂(size₁(y), size₁(z))
+¹₂(0₁(x), 0₁(y)) -> +¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> 0¹₁(-₂(x, y))
MAX₁(n₃(x, y, z)) -> MAX₁(z)
WB₁(n₃(x, y, z)) -> -¹₂(size₁(y), size₁(z))
WB₁(n₃(x, y, z)) -> -¹₂(size₁(z), size₁(y))
BS₁(n₃(x, y, z)) -> AND₂(ge₂(x, max₁(y)), ge₂(min₁(z), x))
+¹₂(0₁(x), 0₁(y)) -> 0¹₁(+₂(x, y))
WB₁(n₃(x, y, z)) -> WB₁(z)
GE₂(1₁(x), 1₁(y)) -> GE₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> -¹₂(x, y)
WB₁(n₃(x, y, z)) -> WB₁(y)
GE₂(#, 0₁(x)) -> GE₂(#, x)
BS₁(n₃(x, y, z)) -> MIN₁(z)
BS₁(n₃(x, y, z)) -> GE₂(min₁(z), x)
BS₁(n₃(x, y, z)) -> AND₂(bs₁(y), bs₁(z))
WB₁(n₃(x, y, z)) -> IF₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y))))
GE₂(0₁(x), 0₁(y)) -> GE₂(x, y)
-¹₂(1₁(x), 1₁(y)) -> -¹₂(x, y)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 9 SCCs with 24 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MAX₁(n₃(x, y, z)) -> MAX₁(z)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

MAX₁(n₃(x, y, z)) -> MAX₁(z)

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
MAX₁(x1) = MAX₁(x1)
n₃(x1, x2, x3) = n₂(x1, x3)

Lexicographic Path Order [19].
Precedence:

n₂ > MAX₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MIN₁(n₃(x, y, z)) -> MIN₁(y)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

MIN₁(n₃(x, y, z)) -> MIN₁(y)

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
MIN₁(x1) = MIN₁(x1)
n₃(x1, x2, x3) = n₁(x2)

Lexicographic Path Order [19].
Precedence:

[MIN₁, n_1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE₂(#, 0₁(x)) -> GE₂(#, x)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

GE₂(#, 0₁(x)) -> GE₂(#, x)

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
GE₂(x1, x2) = GE₁(x2)
# = #
0₁(x1) = 0₁(x1)

Lexicographic Path Order [19].
Precedence:

[#, 0_1] > GE₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE₂(1₁(x), 1₁(y)) -> GE₂(x, y)
GE₂(0₁(x), 0₁(y)) -> GE₂(x, y)
GE₂(1₁(x), 0₁(y)) -> GE₂(x, y)
GE₂(0₁(x), 1₁(y)) -> GE₂(y, x)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

BS₁(n₃(x, y, z)) -> BS₁(y)
BS₁(n₃(x, y, z)) -> BS₁(z)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

BS₁(n₃(x, y, z)) -> BS₁(y)
BS₁(n₃(x, y, z)) -> BS₁(z)

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
BS₁(x1) = BS₁(x1)
n₃(x1, x2, x3) = n₂(x2, x3)

Lexicographic Path Order [19].
Precedence:

n₂ > BS₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

-¹₂(1₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))
-¹₂(1₁(x), 1₁(y)) -> -¹₂(x, y)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

-¹₂(1₁(x), 0₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 0₁(y)) -> -¹₂(x, y)

The remaining pairs can at least by weakly be oriented.

-¹₂(0₁(x), 1₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))
-¹₂(1₁(x), 1₁(y)) -> -¹₂(x, y)

Used ordering: Combined order from the following AFS and order.
-¹₂(x1, x2) = x2
1₁(x1) = x1
0₁(x1) = 0₁(x1)
-₂(x1, x2) = -₁(x2)
# = #

Lexicographic Path Order [19].
Precedence:

-₁ > [0₁, #]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

-¹₂(0₁(x), 1₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))
-¹₂(1₁(x), 1₁(y)) -> -¹₂(x, y)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

-¹₂(0₁(x), 1₁(y)) -> -¹₂(x, y)
-¹₂(0₁(x), 1₁(y)) -> -¹₂(-₂(x, y), 1₁(#))
-¹₂(1₁(x), 1₁(y)) -> -¹₂(x, y)

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
-¹₂(x1, x2) = -¹₂(x1, x2)
0₁(x1) = 0₁(x1)
1₁(x1) = 1₁(x1)
-₂(x1, x2) = x1
# = #

Lexicographic Path Order [19].
Precedence:

[0₁, 1_1] > -^1₂ > #

The following usable rules [14] were oriented:

-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
0₁(#) -> #

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(0₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
+¹₂(1₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(0₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

+¹₂(0₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(x, y)
+¹₂(1₁(x), 0₁(y)) -> +¹₂(x, y)
+¹₂(x, +₂(y, z)) -> +¹₂(+₂(x, y), z)

The remaining pairs can at least by weakly be oriented.

+¹₂(1₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(0₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))

Used ordering: Combined order from the following AFS and order.
+¹₂(x1, x2) = x2
0₁(x1) = 0₁(x1)
1₁(x1) = x1
+₂(x1, x2) = +₂(x1, x2)
# = #

Lexicographic Path Order [19].
Precedence:

[0₁, +_2] > #

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(1₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(0₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

+¹₂(1₁(x), 1₁(y)) -> +¹₂(x, y)
+¹₂(0₁(x), 1₁(y)) -> +¹₂(x, y)

The remaining pairs can at least by weakly be oriented.

+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))

Used ordering: Combined order from the following AFS and order.
+¹₂(x1, x2) = +¹₁(x2)
1₁(x1) = 1₁(x1)
0₁(x1) = 0
+₂(x1, x2) = x1
# = #

Lexicographic Path Order [19].
Precedence:

0 > +^1₁ > 1₁ > #

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(1₁(x), 1₁(y)) -> +¹₂(+₂(x, y), 1₁(#))

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SIZE₁(n₃(x, y, z)) -> SIZE₁(y)
SIZE₁(n₃(x, y, z)) -> SIZE₁(x)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

SIZE₁(n₃(x, y, z)) -> SIZE₁(y)
SIZE₁(n₃(x, y, z)) -> SIZE₁(x)

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
SIZE₁(x1) = SIZE₁(x1)
n₃(x1, x2, x3) = n₂(x1, x2)

Lexicographic Path Order [19].
Precedence:

n₂ > SIZE₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

WB₁(n₃(x, y, z)) -> WB₁(y)
WB₁(n₃(x, y, z)) -> WB₁(z)

The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

WB₁(n₃(x, y, z)) -> WB₁(y)
WB₁(n₃(x, y, z)) -> WB₁(z)

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
WB₁(x1) = WB₁(x1)
n₃(x1, x2, x3) = n₂(x2, x3)

Lexicographic Path Order [19].
Precedence:

n₂ > WB₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

0₁(#) -> #
+₂(x, #) -> x
+₂(#, x) -> x
+₂(0₁(x), 0₁(y)) -> 0₁(+₂(x, y))
+₂(0₁(x), 1₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 0₁(y)) -> 1₁(+₂(x, y))
+₂(1₁(x), 1₁(y)) -> 0₁(+₂(+₂(x, y), 1₁(#)))
+₂(x, +₂(y, z)) -> +₂(+₂(x, y), z)
-₂(x, #) -> x
-₂(#, x) -> #
-₂(0₁(x), 0₁(y)) -> 0₁(-₂(x, y))
-₂(0₁(x), 1₁(y)) -> 1₁(-₂(-₂(x, y), 1₁(#)))
-₂(1₁(x), 0₁(y)) -> 1₁(-₂(x, y))
-₂(1₁(x), 1₁(y)) -> 0₁(-₂(x, y))
not₁(false) -> true
not₁(true) -> false
and₂(x, true) -> x
and₂(x, false) -> false
if₃(true, x, y) -> x
if₃(false, x, y) -> y
ge₂(0₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(0₁(x), 1₁(y)) -> not₁(ge₂(y, x))
ge₂(1₁(x), 0₁(y)) -> ge₂(x, y)
ge₂(1₁(x), 1₁(y)) -> ge₂(x, y)
ge₂(x, #) -> true
ge₂(#, 1₁(x)) -> false
ge₂(#, 0₁(x)) -> ge₂(#, x)
val₁(l₁(x)) -> x
val₁(n₃(x, y, z)) -> x
min₁(l₁(x)) -> x
min₁(n₃(x, y, z)) -> min₁(y)
max₁(l₁(x)) -> x
max₁(n₃(x, y, z)) -> max₁(z)
bs₁(l₁(x)) -> true
bs₁(n₃(x, y, z)) -> and₂(and₂(ge₂(x, max₁(y)), ge₂(min₁(z), x)), and₂(bs₁(y), bs₁(z)))
size₁(l₁(x)) -> 1₁(#)
size₁(n₃(x, y, z)) -> +₂(+₂(size₁(x), size₁(y)), 1₁(#))
wb₁(l₁(x)) -> true
wb₁(n₃(x, y, z)) -> and₂(if₃(ge₂(size₁(y), size₁(z)), ge₂(1₁(#), -₂(size₁(y), size₁(z))), ge₂(1₁(#), -₂(size₁(z), size₁(y)))), and₂(wb₁(y), wb₁(z)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.